$\forall$$x_{1}$:Realizer. ($\uparrow$Rpre?($x_{1}$)) $\Rightarrow$ (Rpre{-}P($x_{1}$) $\in$ State(Rpre{-}ds($x_{1}$))$\rightarrow\mathbb{B}$)